Formal Verification of Deep Brain Stimulation Controllers for Parkinson's Disease Treatment.

Deep brain stimulation (DBS) is a widely accepted treatment for the Parkinson's disease (PD). Traditionally, it is done in an open-loop manner, where stimulation is always ON, irrespective of the patient needs. As a consequence, patients can feel some side effects due to the continuous high-frequency stimulation. Closed-loop DBS can address this problem as it allows adjusting stimulation according to the patient need. The selection of open- or closed-loop DBS and an optimal algorithm for closed-loop DBS are some of the main challenges in DBS controller design, and typically the decision is made through sampling based simulations. In this letter, we used model checking, a formal verification technique used to exhaustively explore the complete state space of a system, for analyzing DBS controllers. We analyze the timed automata of the open-loop and closed-loop DBS controllers in response to the basal ganglia (BG) model. Furthermore, we present a formal verification approach for the closed-loop DBS controllers using timed computation tree logic (TCTL) properties, that is, safety, liveness (the property that under certain conditions, some event will eventually occur), and deadlock freeness. We show that the closed-loop DBS significantly outperforms existing open-loop DBS controllers in terms of energy efficiency. Moreover, we formally analyze the closed-loop DBS for energy efficiency and time behavior with two algorithms, the constant update algorithm and the error prediction update algorithm. Our results demonstrate that the closed-loop DBS running the error prediction update algorithm is efficient in terms of time and energy as compared to the constant update algorithm.

Formalization of bond graph using higher-order-logic theorem proving.

Bond graph is a unified graphical approach for describing the dynamics of complex engineering and physical systems and is widely adopted in a variety of domains, such as, electrical, mechanical, medical, thermal and fluid mechanics. Traditionally, these dynamics are analyzed using paper-and-pencil proof methods and computer-based techniques. However, both of these techniques suffer from their inherent limitations, such as human-error proneness, approximations of results and enormous computational requirements. Thus, these techniques cannot be trusted for performing the bond graph based dynamical analysis of systems from the safety-critical domains like robotics and medicine. Formal methods, in particular, higher-order-logic theorem proving, can overcome the shortcomings of these traditional methods and provide an accurate analysis of these systems. It has been widely used for analyzing the dynamics of engineering and physical systems. In this paper, we propose to use higher-order-logic theorem proving for performing the bond graph based analysis of the physical systems. In particular, we provide formalization of bond graph, which mainly includes functions that allow conversion of a bond graph to its corresponding mathematical model (state-space model) and the verification of its various properties, such as, stability. To illustrate the practical effectiveness of our proposed approach, we present the formal stability analysis of a prosthetic mechatronic hand using HOL Light theorem prover. Moreover, to help non-experts in HOL, we encode our formally verified stability theorems in MATLAB to perform the stability analysis of an anthropomorphic prosthetic mechatronic hand.

A Single-centre Study of COVID-19 Antibody.

ABSTARCT Four hundred and fifty-three SARS CoV-2 antibodies tests were conducted using Roche Elecsys® Anti SARS CoV-2 kits (detecting total antibodies) between June 13 to July 8, 2020 (25 days) on Cobas® e411 automatic analyser, based on electrochemiluminescence immunoassay (ECLIA) principle. Samples were collected from walk-in patients at our facility. Among them, 2 (0.4%) were found equivocal, 289 (63.8%) were found reactive, while 162 (35.8%) were found non-reactive. Moreover, reactive (symptomatic) cases were 262 (57.8%), reactive (asymptomatic) were 27 (6.0%), non-reactive (symptomatic) were 34 (7.5%), while non-reactive (asymptomatic) were 128 (28.3%). Most common symptom was fever, found in 262 (87.9%) individuals, followed by dry cough 146 (49.0%). Most number of reactive cases, i.e. 110 (42.6%) were those who got themselves tested between 15-21 days after onset of first symptom. Key Words: COVID-19, Coronavirus, Antibodies testing.

Chronic kidney disease diagnosis using decision tree algorithms.

BACKGROUND: Chronic Kidney Disease (CKD), i.e., gradual decrease in the renal function spanning over a duration of several months to years without any major symptoms, is a life-threatening disease. It progresses in six stages according to the severity level. It is categorized into various stages based on the Glomerular Filtration Rate (GFR), which in turn utilizes several attributes, like age, sex, race and Serum Creatinine. Among multiple available models for estimating GFR value, Chronic Kidney Disease Epidemiology Collaboration (CKD-EPI), which is a linear model, has been found to be quite efficient because it allows detecting all CKD stages. METHODS: Early detection and cure of CKD is extremely desirable as it can lead to the prevention of unwanted consequences. Machine learning methods are being extensively advocated for early detection of symptoms and diagnosis of several diseases recently. With the same motivation, the aim of this study is to predict the various stages of CKD using machine learning classification algorithms on the dataset obtained from the medical records of affected people. Specifically, we have used the Random Forest and J48 algorithms to obtain a sustainable and practicable model to detect various stages of CKD with comprehensive medical accuracy. RESULTS: Comparative analysis of the results revealed that J48 predicted CKD in all stages better than random forest with an accuracy of 85.5%. The study also showed that J48 shows improved performance over Random Forest. CONCLUSIONS: The study concluded that it may be used to build an automated system for the detection of severity of CKD.

Formal verification of Matrix based MATLAB models using interactive theorem proving.

MATLAB is a software based analysis environment that supports a high-level programing language and is widely used to model and analyze systems in various domains of engineering and sciences. Traditionally, the analysis of MATLAB models is done using simulation and debugging/testing frameworks. These methods provide limited coverage due to their inherent incompleteness. Formal verification can overcome these limitations, but developing the formal models of the underlying MATLAB models is a very challenging and time-consuming task, especially in the case of higher-order-logic models. To facilitate this process, we present a library of higher-order-logic functions corresponding to the commonly used matrix functions of MATLAB as well as a translator that allows automatic conversion of MATLAB models to higher-order logic. The formal models can then be formally verified in an interactive theorem prover. For illustrating the usefulness of the proposed library and approach, we present the formal analysis of a Finite Impulse Response (FIR) filter, which is quite commonly used in digital signal processing applications, within the sound core of the HOL Light theorem prover.

A Single-centre Study of COVID-19 Antibody.

ABSTARCT Four hundred and fifty-three SARS CoV-2 antibodies tests were conducted using Roche Elecsys® Anti SARS CoV-2 kits (detecting total antibodies) between June 13 to July 8, 2020 (25 days) on Cobas® e411 automatic analyser, based on electrochemiluminescence immunoassay (ECLIA) principle. Samples were collected from walk-in patients at our facility. Among them, 2 (0.4%) were found equivocal, 289 (63.8%) were found reactive, while 162 (35.8%) were found non-reactive. Moreover, reactive (symptomatic) cases were 262 (57.8%), reactive (asymptomatic) were 27 (6.0%), non-reactive (symptomatic) were 34 (7.5%), while non-reactive (asymptomatic) were 128 (28.3%). Most common symptom was fever, found in 262 (87.9%) individuals, followed by dry cough 146 (49.0%). Most number of reactive cases, i.e. 110 (42.6%) were those who got themselves tested between 15-21 days after onset of first symptom. Key Words:  COVID-19, Coronavirus, Antibodies testing.

Formal reasoning about synthetic biology using higher-order-logic theorem proving.

Synthetic biology is an interdisciplinary field that uses well-established engineering principles for performing the analysis of the biological systems, such as biological circuits, pathways, controllers and enzymes. Conventionally, the analysis of these biological systems is performed using paper-and-pencil proofs and computer simulation methods. However, these methods cannot ensure accurate results due to their inherent limitations. Higher-order-logic (HOL) theorem proving is proposed and used as a complementary approach for analysing linear biological systems, which is based on developing a mathematical model of the genetic circuits and the bio-controllers used in synthetic biology based on HOL and analysing it using deductive reasoning in an interactive theorem prover. The involvement of the logic, mathematics and the deductive reasoning in this method ensures the accuracy of the analysis. It is proposed to model the continuous dynamics of the genetic circuits and their associated controllers using differential equations and perform their transfer function-based analysis using the Laplace transform in a theorem prover. For illustration, the genetic circuits of activated and repressed expressions and autoactivation of protein, and phase lag and lead controllers, which are widely used in cancer-cell identifiers and multi-input receptors for precise disease detection, are formally analyzed.

Stunting diagnostic and awareness: impact assessment study of sociodemographic factors of stunting among school-going children of Pakistan.

BACKGROUND: Stunting is a major public health issue in most of developing countries. Although, its worldwide prevalence is decreasing slowly but the number of stunted children is still rising in Pakistan. Stunting is highly associated with several long-term consequences, including higher rate of mortality and morbidity, deficient cognitive growth, school performance, learning capacity, work capacity and work productivity. To prevent stunting, we proposed Stunting Diagnostic and Education app. This app includes detailed knowledge of stunting and it's all forms, symptoms, causes, video tutorials and guidelines by the Pediatricians and Nutritionists. METHODS: A cross-sectional study has been conducted in schools of Multan District, Pakistan for the period of January 2019 to June 2019. Sample data of 1420 children, aged 4 to 18 years using three age groups, were analyzed by using SPSS version 21.0 to assess the prevalence of stunting and to analyze the risk factors associated with it in children under and over 5 age. Chi square test was applied in comparison with rural and urban participants and p-value < 0.05 was considered as significant. This study includes distribution of sociodemographic characteristics, parental education, working status of mothers, dietary patterns of school going children and prevalence of stunting in school going children. After getting study results, Stunting Diagnostic and Education app was developed according to the instructions of child experts and nutritionists. RESULTS: 354 (24.93%) participants were stunted out of 1420, 11.9% children were obese and 63.17% children were normal. Out of 354 stunted children, higher ratio of stunting was found in the age group of 8-11 years children with 51.98 percentage. 37.85% stunted children were found in the age group of 4-7 years and 10.17% stunting was found in the age group of 12-18 years children. It was observed in the study that male children were highly stunted than female with 57.91 and 42.09% respectively. Children living in rural areas were more stunted affected as compared to the children living in urban society with percentage 58.76 and 41.24 respectively. CONCLUSIONS: Our study concluded that 24.93% children were stunted, out of which, age group of 8-11 years children were highly stunted. The study showed that the literacy of mother or caregiver had high impact on children's health. Therefore, Stunting Diagnostic and Education app was developed to educate mothers to diagnose stunting and to teach about the prevention of stunting.

How childhood diseases awareness contributes to minimize the risk of disease severity in children under five age: An evolutionary study.

OBJECTIVE: To scrutinise the contribution of childhood disease awareness in mothers to minimise the risk of disease severity in children aged <5 years and to evaluate the effectiveness of a proposed app in this context. METHODS: The evolutionary study was conducted in Children's Hospital and the Institute of Child Health Multan from September 2018 to February 2019 and comprised two sessions with the app involving 30 mothers who were provided with smartphones with the app installed. The mothers were divided into 4 age groups. The app was evaluated using quantitative and qualitative measures. Suggestions and opinions were obtained in the first session and all suggestions were implemented by the second session. RESULTS: Of the 30 mothers, 8(26.6%) were in Group 1 aged 14-20 years, 12(40%) in Group 2 aged 21-27 years, 7(23.3%) in Group 3 aged 28-34 years and 3(10%) in Group 4 aged 35 years and above. The participants were able to diagnose their children's diseases accurately by following the instructions provided by the app. The subjects also agreed that they diagnosed the diseases accurately. All the participants were interested in the app and expressed the desire to have it available across the healthcare facilities in Pakistan. CONCLUSIONS: All subjects showed acceptance for the app and affirmed its easy usability, especially for illiterate mothers.

EasyDetectDisease: An Android App for Early Symptom Detection and Prevention of Childhood Infectious Diseases.

BACKGROUND: Infectious diseases often lead to death among children under 5 years in many underdeveloped and developing countries. One of the main reasons behind this is an unawareness of disease symptoms among mothers and child caregivers. To overcome this, we propose the EasyDetectDisease mobile health app to educate mothers about the early symptoms of pediatric diseases and to provide them with practical advice for preventing the spread of such diseases in children under 5 years. The EasyDetectDisease app includes detailed knowledge of infectious diseases, including the corresponding symptoms, causes, incubation period, preventive measures, nutritional guidelines such as breastfeeding, video tutorials of child patients, and video guidelines by pediatric health experts to promote child health. It also provides information on the diagnosis of the infectious diseases based on symptoms. OBJECTIVE: The objective of this study was to evaluate the usability (eg, ease of use, easy detection of disease, functionality, and navigation of interfaces) of the EasyDetectDisease app among mothers of children under 5 years of age. METHODS: Two health sessions, held in Pakistan, were used to evaluate the usability of EasyDetectDisease by 30 mothers of children under 5 years. The app was evaluated based on various quantitative and qualitative measures. RESULTS: The participating mothers confirmed that they were able to diagnose diseases accurately and that after following the instructions provided, their children recovered rapidly without any nutritional deficiency. All participating mothers showed an interest in using the EasyDetectDisease app if made available by governmental public health agencies, and they suggested its inclusion in all mobile phones as a built-in health app in the future. CONCLUSIONS: EasyDetectDisease was modified into a user-friendly app based on feedback collected during the usability sessions. All participants found it acceptable and easy to use, especially illiterate mothers. The EasyDetectDisease app proved to be a useful tool for child health care at home and for the treatment of infectious diseases and is expected to reduce the mortality rate of children under 5 years of age.

A framework for laparoscopic simulations.

Due to their numerous advantages, laparoscopic surgical procedures are increasingly becoming common in the operation theatres over the past few decades. Virtual reality training simulators have played a significant role during this transition from traditional to laparoscopic procedures by enhancing surgical skills, such as hand-eye coordination in laparoscopy, and practising surgical scenarios that cannot be easily created using physical models. This paper presents a general framework for such a training simulator while identifying its key components and their specific roles in enhancing various laparoscopic skills. The paper also describes a laparoscopic simulator, developed in our lab, based on the proposed framework. The results are promising and open new doors for research and development.

Formal reasoning about systems biology using theorem proving.

System biology provides the basis to understand the behavioral properties of complex biological organisms at different levels of abstraction. Traditionally, analysing systems biology based models of various diseases have been carried out by paper-and-pencil based proofs and simulations. However, these methods cannot provide an accurate analysis, which is a serious drawback for the safety-critical domain of human medicine. In order to overcome these limitations, we propose a framework to formally analyze biological networks and pathways. In particular, we formalize the notion of reaction kinetics in higher-order logic and formally verify some of the commonly used reaction based models of biological networks using the HOL Light theorem prover. Furthermore, we have ported our earlier formalization of Zsyntax, i.e., a deductive language for reasoning about biological networks and pathways, from HOL4 to the HOL Light theorem prover to make it compatible with the above-mentioned formalization of reaction kinetics. To illustrate the usefulness of the proposed framework, we present the formal analysis of three case studies, i.e., the pathway leading to TP53 Phosphorylation, the pathway leading to the death of cancer stem cells and the tumor growth based on cancer stem cells, which is used for the prognosis and future drug designs to treat cancer patients.

SmartSIM - a virtual reality simulator for laparoscopy training using a generic physics engine.

Virtual reality (VR) training simulators have started playing a vital role in enhancing surgical skills, such as hand-eye coordination in laparoscopy, and practicing surgical scenarios that cannot be easily created using physical models. We describe a new VR simulator for basic training in laparoscopy, i.e. SmartSIM, which has been developed using a generic open-source physics engine called the simulation open framework architecture (SOFA). This paper describes the systems perspective of SmartSIM including design details of both hardware and software components, while highlighting the critical design decisions. Some of the distinguishing features of SmartSIM include: (i) an easy-to-fabricate custom-built hardware interface; (ii) use of a generic physics engine to facilitate wider accessibility of our work and flexibility in terms of using various graphical modelling algorithms and their implementations; and (iii) an intelligent and smart evaluation mechanism that facilitates unsupervised and independent learning.